Nuprl Lemma : priority-select_wf
11,40
postcript
pdf
T
:Type,
as
:(
T
List),
f
,
g
:(
T
). priority-select(
f
;
g
;
as
)
(?
)
latex
Definitions
t
T
,
,
Unit
,
ff
,
x
:
A
.
B
(
x
)
,
if
b
then
t
else
f
fi
,
tt
,
isl(
x
)
,
,
x
,
y
.
t
(
x
;
y
)
,
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
,
priority-select(
f
;
g
;
as
)
Lemmas
list
accum
wf
,
it
wf
,
isl
wf
,
btrue
wf
,
ifthenelse
wf
,
bfalse
wf
,
unit
wf
,
bool
wf
origin
T:Type, as:(T List), f,g:(T
). priority-select(f; g; as) 
(?) T:Type, as:(T List), f,g:(T). priority-select(f; g; as) (?) Tx:A. B(x)
x,y. t(x;y)